$\forall$$T$:Type, ${\it as}$, ${\it as'}$, ${\it bs}$, ${\it cs}$:$T$ List.
\\[0ex]$\parallel$${\it as}$$\parallel$ $=$ $\parallel$${\it as'}$$\parallel$ $\in$ $\mathbb{Z}$ $\Rightarrow$ (${\it as}$ @ ${\it cs}$) $=$ (${\it as'}$ @ ${\it bs}$) $\in$ $T$ List $\Rightarrow$ ${\it cs}$ $=$ ${\it bs}$